Tuesday, June 11, 2002, 2:00 PM - 4:00 PM | Room: 292 SESSION 8    Formal Verification    Chair: Yaron Wolfsthal - IBM Corp., Haifa, ISR    Organizers: Carl Pixley, Karem Sakallah    The need and benefits of formal verification (FV) have been accepted for some time. The capacity of FV-based tools is still limited and in this session new technologies and methodologies are presented that enable larger designs to be formally verified. In particular, novel ideas to enhance symbolic simulation, hybrid approach that uses symbolic simulation and model checking and SAT and BDD bounded model-checking.      8.1 Efficient State Representation for Symbolic Simulation    Speaker(s): Valeria Bertacco - Stanford Univ., Stanford, CA    Author(s): Valeria Bertacco - Stanford Univ., Stanford, CA Kunle Olukotun - Stanford Univ., Stanford, CA      8.2 Handling Special Constructs in Symbolic Simulation    Speaker(s): Alfred Koelbl - Tech. Univ. of Munich, Munich, Germany    Author(s): Alfred Koelbl - Tech. Univ. of Munich, Munich, Germany James Kukula - Synopsys, Inc., Beaverton, OR Kurt Antreich - Tech. Univ. of Munich, Munich, Germany Robert Damiano - Synopsys, Inc., Beaverton, OR      8.3 A Hybrid Verification Approach: Getting Deep into the Design    Speaker(s): Scott Hazelhurst - Univ. of the Witwatersrand, Johannesburg, S. Africa    Author(s): Scott Hazelhurst - Univ. of the Witwatersrand, Johannesburg, S. Africa Osnat Weissberg - Intel Corp., Haifa, Israel Gila Kamhi - Intel Corp., Haifa, Israel Limor Fix - Intel Corp., Haifa, Israel      8.4 Can BDDs Compete with SAT Solvers on Bounded Model Checking?    Speaker(s): Gianpiero Cabodi - Politecnico di Torino, Turin, Italy    Author(s): Gianpiero Cabodi - Politecnico di Torino, Turin, Italy Paolo E. Camurati - Politecnico di Torino, Turin, Italy Stefano Quer - Politecnico di Torino, Turin, Italy